es:ES, ff:FIFO, i:ff.C, e, e':{e:E| ff.R(i,e)} , j:ff.C.
(ff.S(j,i,ff.Sender(i,e)))
 (ff.S(j,i,ff.Sender(i,e')))
 e c e'
 ((ff.Sender(i,e') < ff.Sender(i,e))) 

latex

Definitions	x:A. B(x), FIFO, P  Q, t  T, , x:A. B(x), A, False, e c e', P  Q
Lemmas	es-causle wf, fifoS wf, fifoSender wf, es-E wf, fifoC wf, fifoR wf, es-state wf, es-loc wf, fifo wf, event system wf, es-causl wf, fifoSender-preserves-order, es-causle weakening, es-causl irreflexivity, es-causl transitivity2